T:Type, L:(T List), P:(T).
l_all(L; T; x.(P(x)))  (reduce((x,y. band(P(x); y)); tt; L)) 

latex

Definitions	t  T, if b then t else f fi , Y, tt, reduce(f; k; as), b, x:A. B(x), x. t(x), prop{i:l}, P  Q, P  Q, P  Q, True, x(s), P  Q
Lemmas	bool wf, true wf, l all nil, l member wf, assert wf, l all wf, l all cons, assert of band, iff functionality wrt iff, all functionality wrt iff, btrue wf, reduce wf, band wf, iff wf